\documentclass[a4paper,10pt]{article}

% Modification de la géométrie de la page
\setlength{\textheight}{21cm} % hauteur utile de texte sur la page
\setlength{\textwidth}{15cm}  % largeur utile de texte sur la page
\setlength{\hoffset}{-1.5cm}  % marge supérieure

% Packages pour la langue
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}

% Packages pour les maths
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{proof}
\usepackage{amsthm}
\usepackage{cmll}
\usepackage{amssymb}
\usepackage{amscd}
\usepackage{latexsym}
\usepackage{txfonts}
\usepackage{graphicx}


% Packages pour étendre les fonctionnalités des tableaux en latex
\usepackage{array}
\usepackage{booktabs}

% ---- Macros ----

% Logique
\newcommand{\impl}{\rightarrow}	% ->
\newcommand{\limpl}{\multimap}  % -o
\newcommand{\pnet}{\mathcal{R}} % R proof-net

% Général
\newcommand{\Nset}{\mathbb{N}} % N ens des entiers

% Théorie de la complexité
\newcommand{\Mnice}{\mathcal{M}}			 % M Turing machine
\newcommand{\clFP}{\textbf{FP}}				 % Classe FP
\newcommand{\clP}{\textbf{P}}				 % Classe P
\newcommand{\clElem}{\textbf{Elem}}			 % Classe Elem
\newcommand{\clFExpT}{\textbf{FExpTime}}	 % Classe FExpTime


% Macros pour les paragraphes:
\newtheorem{definition}{Definition}
\newtheorem{prop}{Property}
\newtheorem{thm}{Theorem}
\newtheorem{lem}{Lemma}
\newtheorem{ex}{Example}
\newtheorem{exo}{Exercise}
\newtheorem{rmk}{Remark}

% Infos sur le documents
\author{Patrick Baillot \and Paulin Jacobé de Naurois \and (transcribed by the students)}
\title{CR04 - Implicit complexity} 



\begin{document}

\maketitle

\part{Linear Logic}

\subsection{Deterministic Turing Machines}

\par Let $f:\{0;1\}^{*} \mapsto \{0;1\}^{*}$. We say that $\Mnice$ \emph{represents} $f$ iff, on input $x$, $\Mnice$ terminates after a finite number of steps, with $y=f(x)$ written on the output tape.

\par Then, we define $\clFP$ as the set of function $f:\{0;1\}^{*} \mapsto \{0;1\}^{*}$ computable by a Turing machine in a polynomial time in the size of its input. We also define $\clP$ as the set of function $f:\{0;1\}^{*} \mapsto \{0;1\}$ which verify the same conditions.

\begin{definition}
The class $\clElem$ of \emph{elementary functions} is the set of functions which are computable by a Turing Machine in time $O(2^{\dots ^{2^n}}$, with $d$ power of 2, where $d$ is fixed (does not depend of n).
\end{definition}

\par Therefore, we have $\clFExpT \subseteq \clElem \subseteq$ primitive recursive functions. $\clElem$ can also be characterized as a class of functions: it is the smallest class of function $\Nset^{k} \mapsto \Nset$ which:
\begin{itemize}
\item contains some basic functions (0, Succ, projections...)
\item is closed by schemes of bounded sums and products.
\end{itemize}



\subsection{System F of polymorphic types}

\begin{definition}
\item Terms of $\lambda$-calculus: $t,u,... \Coloneqq x | (t u) | \lambda x.t$
\item System F types: $A,B,... \Coloneqq \alpha | A\impl B | \forall \alpha .A $
\item Type judgments: $x_1:A_1, ..., x_n:A_n \vdash t:A$
\end{definition}

\par The typing rules for system F are:
$$	\infer[(ax)]{x:A \vdash x:A}{} \quad
	\infer[(\limpl_i)]{\Gamma \vdash \lambda x.t : A \limpl B}{\Gamma, x:A \vdash t:B} \quad
	\infer[(\limpl_e)]{\Gamma \vdash (t u) : B}{\Gamma \vdash t : A \limpl B & \Gamma \vdash u : A }$$ \\
$$	\infer[(\forall_i), \alpha \notin FV(\Gamma)]{\Gamma \vdash t:\forall \alpha.A}{\Gamma \vdash t:A} \quad
	\infer[(\forall_e)]{\Gamma \vdash t:A[B/\alpha]}{\Gamma \vdash t:\forall \alpha.A}
$$

\begin{rmk}
These rules corresponds by Curry-Howard to natural deduction in second order intuitionistic logic
\end{rmk}

\begin{ex}
$$ \infer[(\forall_e) (B=\forall \alpha.(\alpha \impl \alpha))]{\vdash \lambda x. x: (\forall \alpha. \alpha \impl \alpha) \impl (\forall \alpha. \alpha \impl \alpha)}
	{
	\infer[(\forall_i)]{\vdash \lambda x.x : \forall \alpha.(\alpha \limpl \alpha)}
		{
		\infer[(\limpl_i)]{\vdash \lambda x.x : \alpha \limpl \alpha}
			{
				\infer{x:\alpha \vdash x:\alpha}{}
			}
		}
	}$$
\end{ex}



\subsection{Data types}

\begin{definition}
\item Boolean Bool: $\forall \alpha.(\alpha \impl \alpha \impl \alpha)$
\item Unary (Church) Integers: $N = \forall \alpha.(\alpha \impl \alpha) \impl (\alpha \impl \alpha)$
\item[$\rightarrow$] $\underbar{n} = \lambda f x. f\dots f x$, with $n$ applications of $f$.
\item Binary words: $W = \forall \alpha.(\alpha \impl \alpha) \impl (\alpha \impl \alpha) \impl (\alpha \impl \alpha)$
\item[$\rightarrow$] $<1,0,0> = \lambda s_0 s_1 x. s_1 s_0 s_0 x$.
\vspace{0.2cm}

\item Iterators: $iter^{N} = \lambda step base n. (n step base) : (A \impl A) \impl A \impl N \impl A$
\item[$\rightarrow$] $iter^{N} step base n \mapsto^{*} (step \dots step base)$, with $n$ $step$.
\item $iter^{W} = \lambda step_0 step_1 base w. (w step_0 step_1 base) : (A \impl A) \impl (A \impl A) \impl A \impl W \impl A$
\item[$\rightarrow$] $iter^{W} step_0 step_1 base <1,0,0> \mapsto^{*} step_1 step_0 step_0 base$
\end{definition}

\begin{ex}[Examples of terms]
\item Addition: $add = \lambda n m f x.(m f (n f x))$
\item Multiplication: $mult = \lambda n m f. (m (n f)) = \lambda n m.(iter^N (add n) \underbar{0}) m$
\item Concatenation: $conc = \lambda w w' s_0 s_1 x. (w s_0 s_1 (w' s_0 s_1 x)) : W \impl W \impl W$
\item Length: $\lambda w f x.(w f f w): W \impl N$
\item Exp: $\lambda n. iter double 1 n : N \impl N$
\item t: $\lambda n.iter^N exp 1 n: N \impl N$ represents a non-elementary function.
\end{ex}

\begin{prop}[Subject reduction]
If $\Gamma \vdash t:A$ and $t \rightarrow^{*} t'$, then $\Gamma \vdash t':A$
\end{prop}

\begin{thm}[Girard 1972]
If $t$ is typable in system F, then it is strongly normalizing.
\end{thm}

\par Therefore, a type derivation in F is a kind of termination certificate. In particular, if $\vdash W \impl W$ is derivable in system F, then for any word $w \in \{0;1\}^{*}$, $t \underbar{w}$ terminates, where $\underbar{w}$ represent $w$.

\par Can we refine this kind of certificate in order to ensure complexity bounds instead of termination ?


% -----------------------------------------------------------------------------------------------------

\newpage

% ------ Chap 1 : ELL
\section{Elementary Linear Logic}

\subsection{Introduction:}
In normalization, cut-elimination and $\beta$-reduction, the complexity arises from the duplication of subproofs. To tame the complexity, one possible way is to control duplication. For this, we will use the linear logic.

$A \impl B \equiv ! A \limpl B$, with $\impl$ the intuitionistic implication, $\limpl$ the linear arrow and $!$ the bang connective (which control duplication).

$A \limpl B$ means that A is used exactly one time in the proof/program. On the opposite, $!A$ means that the formula $A$ can be duplicated or erased at will. The sequent-calculus rules related to the $!$ are:
\begin{center}
$	\infer[(contraction)]{!A, \Gamma \vdash B}{!A, !A, \Gamma \vdash B} \quad
	\infer[(weakening)]{!A, \Gamma \vdash B}{\Gamma \vdash B} \quad
	\infer[(promotion)]{!A_{1}, ... , !A_{n} \vdash !A }{!A_{1}, ... , !A_{n} \vdash A}
$
\end{center}

 Linear logic is at least as expressive as system F. The idea is to constraint duplication to have a complexity bound. For that, we have to make "$!$" less powerful $\Rightarrow$ we define a weaker "$!$" connective.


\subsection{Elementary Linear Logic (ELL)}
 We define the types of ELL as: $A,B \Coloneqq \alpha \ | \ A \limpl B \ | \ !A \ | \ \forall \alpha.A \ | \ A \otimes B \ $ (but we won't use this last operator). The typing judgments are on the form: $x_1 : A_1, ..., x_n : A_n \vdash t:B$. We give rules in natural deduction style:
\begin{center}
$	\infer[(ax)]{x:A \vdash x:A}{} \quad
	\infer[(\limpl_i)]{\Gamma \vdash \lambda x.t : A \limpl B}{\Gamma, x:A \vdash t:B} \quad
	\infer[(\limpl_e)]{\Gamma_1, \Gamma_2 \vdash (t_1 t_2) : B}{\Gamma_1 \vdash t_1 : A \limpl B & \Gamma_2 \vdash t_2 : A }$\\
\vspace{0.2cm}
$	\infer[(\forall_i), \alpha \notin FV(\Gamma)]{\Gamma \vdash t:\forall \alpha.A}{\Gamma \vdash t:A} \quad
	\infer[(\forall_e)]{\Gamma \vdash t:A[B/\alpha]}{\Gamma \vdash t:\forall \alpha.A}
$
\end{center}

In binary rules, we assume that $\Gamma_1 \cap \Gamma_2 = \emptyset$ (no common variable). Thus, we obtain the \emph{Intuitionistic multiplicative linear logic (IMLL)}.


In IMLL, if $t$ is typable, then any variable in $t$ occurs at least once. Moreover, the $\beta$-reduction can be performed in a linear number of steps. However, we cannot represent Church Integers in IMLL. To get ELL, we add to IMLL the following typing rules:

\begin{center}
$	\infer[(contr)]{x:!A, \Gamma \vdash t[x/x_1][x/x_2]:B}{x_1 : !A, x_2 : !A, \Gamma \vdash t : B } \quad
	\infer[(weak)]{\Gamma, x:!A \vdash t : B}{\Gamma \vdash t:B}$ \\
	\vspace{0.5cm}
$	\infer[(!_i)]{x_1 : !A_1, ..., x_n : !A_n \vdash t : !B}{x_1 : A_1, ..., x_n : A_n \vdash t : B} \quad
	\infer[(!_e)]{\Gamma_1, \Gamma_2 \vdash u[t/x] : B}{\Gamma_1 \vdash t:!A  &  x:!A,\Gamma_2 \vdash u:B}
$
\end{center}

 We can notice that linear logic is more general than ELL. Moreover, we have an extra rule in linear logic:
\begin{center}
$\infer[(dereliction)]{!A, \Gamma \vdash B}{A, \Gamma \vdash B }$
\end{center}

 By using the dereliction and the promotion, we can derive the $(!i)$ rule of ELL. However, $(!A \limpl A)$ and $(!A \limpl !!A)$ are provable in linear logic, and not in ELL.

 If we add the general weakening rule to ELL, we obtain a new system called \emph{Elementary Affine Logic (EAL)}. This rule is:
\begin{center}
$\infer[(gen.weak)]{x:A, \Gamma \vdash t:B}{\Gamma \vdash t:B }$
\end{center}

Almost all properties that we will see for ELL are also valid for EAL.

\begin{definition}
$!^k A = !...! A$, with k $!$.
\end{definition}



\subsection{Forgetful map}

\begin{definition}[Forgetful map]
 We define the function $(.)^{-} : ELL \mapsto F$ by induction with:\\
$(!A)^{-} = A^{-}$, $(A \limpl B)^{-} = A \impl B$, $\alpha^{-} = \alpha$ and $(\forall \alpha.A)^{-} = \forall \alpha.A^{-}$.
\end{definition}

\begin{prop}
 If $\Gamma \vdash_{ELL} t:A$ is derivable in ELL, then $\Gamma^{-} \vdash_{F} t:A^{-}$ in F
\end{prop}
\begin{proof}
By induction on the ELL derivation. Just note that the following rules are derivable in F:\\
$	\infer{\Gamma_1 , \Gamma_2 \vdash (t_1 t_2):B}{\Gamma_1 \vdash t_1 :A \impl B & \Gamma_2 \vdash t_2 : A } \quad
	\infer{\Gamma, x:A \vdash t[x/x_1 , x/x_2] : B}{x_1 :A, x_2 :A, \Gamma \vdash t:B} \quad
	\infer{\Gamma , x:A \vdash t : B}{\Gamma \vdash t : B} \quad
	\infer{\Gamma_1, \Gamma_2 \vdash u[t/x] : B}{\Gamma_1 \vdash t:A  &  x:A,\Gamma_2 \vdash u:B} $
\end{proof}

\begin{definition}[Decoration]
If $T$ is a type of system F and $A$ is a type of ELL, with $A^{-}=T$, we say that $A$ is a \textbf{decoration} of $T$.
\end{definition}

\begin{rmk}
The system we call here ELL is often called intuitionistic elementary linear logic (there is also "classical" elementary linear logic).
\end{rmk}



\subsection{Data-types}

\begin{center}
\begin{tabular}{|c|c|}
\hline
ELL & System F \\
\hline
$N^{ELL} = \forall \alpha. !(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha)$ & $N^{F} = \forall \alpha. (\alpha \impl \alpha) \impl (\alpha \impl \alpha)$\\
\hline
$W^{ELL} = \forall \alpha. !(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha)$ & $W^{F} = \forall \alpha. (\alpha \impl \alpha) \impl (\alpha \impl \alpha) \impl (\alpha \impl \alpha)$\\
\hline
\end{tabular}
\end{center}


\begin{ex}{Type derivation of $\vdash_{ELL} \underbar{3}:N$}

$$ \infer[(\forall_i) (\limpl_e)]{\vdash \lambda f x.(f f f x) : N^{ELL}}
	{
	\infer[(contr) (contr)]{f: !(\alpha \limpl \alpha) \vdash \lambda x.(f f f x) : !(\alpha \limpl \alpha)}
		{
		\infer[(!_i) (\limpl_i)]{1 \leq i \leq 3, f_i: !(\alpha \limpl \alpha) \vdash \lambda x. (f_1 f_2 f_3 x) : !(\alpha \limpl \alpha)}
			{
				\infer{1 \leq i \leq 3, f_i: !(\alpha \limpl \alpha) \vdash f_1 f_2 f_3 x : \alpha}
				{(To do)}
			}
		}
	}$$
\end{ex}

\begin{rmk}
Note that $(N^{ELL})^{-} = N^{F}$ and $(W^{ELL})^{-} = W^{F}$. We will write $N$ (resp. $W$) instead of $N^{ELL}$ and $W^{ELL}$.\\
Notation: $N_A = !(A \limpl A) \limpl !(A \limpl A)$
\end{rmk}

\begin{exo}
Write the type derivation in ELL for $\vdash_{ELL} \underbar{101} : W$, where $\underbar{101} = \lambda s_0 s_1 x. (s_1 s_0 s_1 x)$.
\end{exo}

 Some examples of typed terms:\\
$add = \lambda n. \lambda m. \lambda f. \lambda x. (n f (m f) x) : N \limpl N \limpl N$\\
$mult = \lambda n. \lambda m. \lambda f. (n (m f)) : N \limpl N \limpl N$\\
$square = \lambda n. \lambda f. (n (n f)) : N \limpl N$.

 Some example of type derivation: addition.\\
\vspace{0.3cm}
\hspace{-1.5cm}
\begin{small}
$ \infer[(\forall_i)]{n:N, m:N \vdash \lambda f x.(n f (m f) x) : N}
	{
	\infer[(\limpl_i)]{n:N , m:N \vdash \lambda f x. t : !(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha)}
	{
	\infer[(contr)]{n:N , m:N, f:!(\alpha \limpl \alpha) \vdash \lambda x.t : !(\alpha \limpl \alpha)}
		{
			\infer{n:N , m:N, f_1:!(\alpha \limpl \alpha), f_2:!(\alpha \limpl \alpha) \vdash \lambda x. (n f_1 (m f_2) x) : !(\alpha \limpl \alpha)}
			{
			\infer{n:N, f_1:!(\alpha \limpl \alpha) \vdash (n f_1):!(\alpha \limpl \alpha)}
				{
				\infer{n:N \vdash n:!(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha)}{\infer{n:N \vdash n:N}{}}
				&
				\infer{f_1:!(\alpha \limpl \alpha) \vdash f_1:!(\alpha \limpl \alpha)}{}
				}
			&
			\infer{y_1,f_2:!(\alpha \limpl \alpha), m:N \vdash \lambda x.(y_1 (m f_2 x)): !(\alpha \limpl \alpha)}
				{
				\infer{m:N, f_2:!(\alpha\limpl\alpha) \vdash m f_2 : !(\alpha \limpl \alpha)}{ \dots }
				&
				\infer[!_i]{y_1, y_2:!(\alpha \limpl \alpha) \vdash \lambda x. (y_1 y_2 x):!(\alpha \limpl \alpha)}
					{
					\infer{y_1, y_2:(\alpha \limpl \alpha) \vdash \lambda x. (y_1 y_2 x):(\alpha \limpl \alpha)}{ \dots } 
					}
				}
			}
		}
	}
	}$
\end{small}

\begin{exo}
Write the type derivation for mult.
\end{exo}

 Type derivation for square:
\begin{center}
$	\infer[\limpl_i]{\vdash square: !N \limpl !N}{
		\infer[contr]{k:!N \vdash \lambda f.(k (k f)): !N}{
			\infer[!_i]{n,m:!N \vdash \lambda f.(n (m f)): !N}{
				\infer{n,m:N \vdash \lambda f.(n (m f)): N}{ (exo) }
			}
		}
	}$
\end{center}

\begin{prop}
If $\Gamma \vdash_{ELL} t:A$ and $t \rightarrow t'$ where $t'$ is in $\beta$ normal form, then we have $\Gamma \vdash t':A$.
\end{prop}

\begin{rmk}
In general, if $t \rightarrow t'$ by one reduction step, we do not have $\Gamma \vdash t':A$
\end{rmk}

\begin{exo}
Find a counter-example
\end{exo}

\begin{thm}
If $\vdash_{ELL} t:N \limpl !^{k} N$, then $t$ represent an elementary function.\\
Conversely, if $f: \Nset \mapsto \Nset$ is an elementary function, then there exist $k\in \Nset$ and a term $t$ such that $t$ represents $f$ and $\vdash_{EAL} t:N\limpl !^{k}N$
\end{thm}


\subsection{Proof-nets}

 To prove the complexity bound, we will use a graphical representation for the typed terms proof nets. We use proof-nets for ELL.
\begin{center}
	\vspace{-0.3cm}
	\includegraphics[scale=0.5]{figures/trad_deriv_pn.pdf}
\end{center}

 We define the ELL proof-nets by induction: each construction step corresponds to a typing rules. Each node has a principal port marked with a $\bullet$.
\begin{figure}[h]
	\begin{center}
		\includegraphics[height=0.36\textheight]{figures/ell.pdf}
		\caption{ELL-proof-nets}
	\end{center}
\end{figure}

\begin{ex}[Example of proof-net]

\begin{figure}[h]
   \begin{minipage}[c]{.46\linewidth}
      \includegraphics[width=0.8\linewidth]{figures/three.pdf}
      \caption{Derivation for $\vdash 3:N$}
   \end{minipage} \hfill
   \begin{minipage}[c]{.46\linewidth}
      \includegraphics[width=0.7\linewidth]{figures/add.pdf}
      \caption{Derivation for addition: $n,m:\ !n \vdash \lambda f x. ((n f) (m f) x): N$}
   \end{minipage}
\end{figure}

\end{ex}


\subsection{Proof-nets reduction}

 A \textbf{cut} is an edge between 2 principal ports. To reduce the cuts in a proof-net, we use the reduction steps described by figure~\ref{fig:cut}.

\begin{figure}
	\begin{center}
		\includegraphics[width=0.8\textwidth]{figures/cut.pdf}
		\caption{The cut-reduction steps}
		\label{fig:cut}
	\end{center}
\end{figure}

\begin{prop}
	If $\pnet = \Pi^{*}$ where $\Pi$ is a derivation of $\Gamma \vdash_{ELL} t:A$, and $\pnet \rightarrow \pnet'$.\\
	Then, there exist $\Pi'$ derivation of $\Gamma \vdash_{ELL} t':A$ with [$t \rightarrow_{\beta} t'$ or $t=t'$] and $(\Pi')^{*}=\pnet'$.
\end{prop}

\begin{prop}
	If $\pnet = \Pi^{*}$ where $\Pi$ is a derivation of $\Gamma \vdash_{ELL} t:A$ and if $\pnet$ is on normal form, then $t$ is on normal form.
\end{prop}

\begin{exo}\label{ex:term}
Reduce and find the related terms of figure~\ref{fig:exo4}.
\begin{figure}[h]
\begin{center}
	\includegraphics[width=0.4\textwidth]{figures/exo1.pdf}
	\caption{Exercise~\ref{ex:term}.}
	\label{fig:exo4}
\end{center}
\end{figure}
\end{exo}

\begin{rmk}[Equivalent representation]
 The proof nets construction are related to those presented in CR02:

\begin{center}
	\begin{minipage}[c]{.46\linewidth}
    	\includegraphics[width=0.8\textwidth]{figures/pn_equiv_representation.pdf}
	\end{minipage} \hfill
	\begin{minipage}[c]{.46\linewidth}
	\begin{tabular}{|c|c|}
		\hline
		$\lambda$-node & $r$-node \\
		\hline
		@-node & $\otimes$-node \\
		\hline
		$\relbar$ & axiom node \\
		$\multimapdotboth$ & cut node \\
		\hline
	\end{tabular}
	\end{minipage}
\end{center}
\end{rmk}

\begin{exo}
	Take the proof-net of Add, and apply it to $\underbar{2}$ and $\underbar{3}$ to get $\underbar{5}$.
\end{exo}

\begin{prop}[Stratification]
	The depth of an edge does not change during a reduction step.
\end{prop}

\begin{definition}
	We define the function $K$ such as $K(0,n)=n$ and $K(k+1,n) = 2^{K(k,n)}$.
\end{definition}

\begin{thm}
	Let $\pnet$ be an ELL proof-net of depth $d$. Then, the reduction of $\pnet$ into its normal form can be done in a number of steps, bounded by $K(d+1, |\pnet|)$.
\label{ComplexityThm}
\end{thm}

\begin{definition}
	An \textbf{exponential tree} of a proof-net $\pnet$ is a subgraph of $\pnet$ which is a tree with:
		\begin{itemize}
			\item Internal nodes, which are contraction
			\item Leaves, which are (!L) nodes or (W) nodes
		\end{itemize}
\end{definition}

\begin{definition}
	An \textbf{active node} is a contraction node, a (!L) node or a (W) node belonging to an exponential tree whose root-edge is a cut.
\end{definition}

\begin{definition}
 Let $\pnet$ be a proof-net, without cuts at depths $\leq (i-1)$, and with exactly one exponential cut at depth $i$. We define the relation $<_{1}$ on the (!R) nodes at depth $i$ by: $N_1 <_{1} N_2 \Leftrightarrow $
\begin{center}
	\includegraphics[scale=0.7]{figures/lt1.pdf}
\end{center}


 Let $<$ be the reflexive and transitive closure of $<_1$.

\end{definition}

\begin{lem}
	$<$ is a partial order on the (!L) nodes at depth i.
\end{lem}
\begin{proof}
	Because of the correction criterion, we have an acyclic condition.
\end{proof}

\subsection{Reduction strategy:}
 Among the increasing depths $i$, i-round:
\begin{itemize}
	\item Phase a: We suppress the $\lambda/@$-cuts and the $\forall$-cuts
	\item Phase b: We suppress a maximal exponential cut, until there is no more exponential cut.
\end{itemize}

\begin{rmk}
	During the phase a, the number of nodes is decreasing. During the phase b, the number of active nodes is decreasing.
\end{rmk}
% FIXME : preuve complète ?
% Guillaume: Je l'ai pas sur mon cours. Après, c'étais le cours en plus du Jeudi, et je n'étais pas là. Du coup, j'ai rattrapé sur Lucien. Donc, si tu as une preuve à cet endroit, n'hésite pas à la mettre...

\begin{lem}
	\begin{itemize}
		\item If $\pnet$ is a proof-net at the beginning of a i-round, then $length(i-round) \leq 2 |\pnet|$.
		\item $|\pnet^{(i)}|_{(i+1)} \leq 2^{\dots^{2^{|\pnet|}}} = K(i+1, |\pnet|)$, with $(i+1)$ power of $2$.
	\end{itemize}
\end{lem}

 Conclusion: the number of step is $S \leq \sum_{i=0}^{d} 2.K(i,|\pnet|) \leq 2.(d+1).K(d,|\pnet|) \leq K(d+1,|\pnet|)$. Therefore, we have the proof of thm~\ref{ComplexityThm}.

\subsection{Representation of a function:}

\begin{definition}
If $\vdash_{ELL} t: N \limpl !^{k} N$, then $t$ \textbf{represents} $f:\Nset \mapsto \Nset$ iff $(\forall n) (t n)$ reduces itself into $f(n)$.
\end{definition}

\begin{prop}
If $\vdash_{ELL} t:N \limpl !^{k} N$, then t represents an elementary function.
\end{prop}

\begin{prop}
	If $f: \Nset \mapsto \Nset$ is an elementary function, then $f$ is representable in EAL.\\
	That is to say: $\exists k \in \Nset, t$ term, such that: $\Gamma \vdash_{EAL} t: N \limpl !^{k} N$ and $t$ computes $f$.
\end{prop}
\begin{proof}
	Admitted
\end{proof}


\subsection{Iteration in ELL}

 We define the iteration of the type N, as in system F: $iter^N = \lambda f x n. (n f x) : !(A \limpl A) \limpl !A \limpl N \limpl !A$, for any $A$.\\
Therefore, $iter^N step base n \rightarrow step \dots step base$, with $n$ $step$.\\
Its type derivation is:
\begin{center}
$	\infer[(\limpl_i) (\limpl_i) (\limpl_i)]{\vdash iter^N: !(A \limpl A) \limpl !A \limpl N \limpl !A}{
		\infer[(!_e)]{f:!(A \limpl A), x:!A, n:N \vdash (n f x): !A}{
			\infer{n:N, f:!(A \limpl A) \vdash n f: !(A \limpl A)}{
				\infer[(\forall_e)]{n:N \vdash n: !(A\limpl A) \limpl !(A \limpl A)}{
					\infer[(ax)]{n:N \vdash n:N}{}
				}
				&
				\infer[(ax)]{f:!(A\limpl A) \vdash f:!(A\limpl A)}{}
			}
			&
			\infer[(!_i)]{y:!(A\limpl A), x:!A \vdash y x:!A}{
				\infer[(\limpl_e)]{y:A\limpl A, x:A \vdash y x:A}{
					\infer[(ax)]{y:A\limpl A \vdash y:A \limpl A}{}
					&
					\infer[(ax)]{x:A \vdash x:A}{}
				}
			}
		}
	}$
\end{center}

\begin{ex}
\begin{itemize}
\item $mult: N \limpl N \limpl N$
\item $double=(mult\ 2): N \limpl N$
\item $exp=iter^N double 1: N \limpl !N$
\item $tower=iter^N exp 1$ is not typable in ELL ($N\limpl !N \neq A\limpl A$).
\item Derivation of exp:
\begin{center}
$	\infer{\vdash iter^N double 1: N \limpl !N}{
		\infer{\vdash iter^N double: !N \limpl N \limpl !N}{
			\infer{\vdash iter^N: !(N\limpl N) \limpl !N \limpl N \limpl !N}{}
			&
			\infer[(!i)]{\vdash double:!(N\limpl n)}{\vdash double:N\limpl N}
		}
		&
		\infer{\vdash 1:!N}{\infer{\vdash 1:N}{}}
	}$
\end{center}

\item $2exp= \lambda x.(exp exp x): N \limpl !!N$ (represent $2^{2^{n}}$). Type derivation:
\begin{center}
$	\infer[(!_e)]{x:N \vdash exp exp x: !!N}{
		\infer{x:N \vdash exp x: !N}{\vdash exp:N \limpl !N}
		&
		\infer[(!_i)]{y:!N \vdash exp y:!!N}{y:N \vdash exp y:!N}
	}$
\end{center}
\end{itemize}

\end{ex}


\subsection{Coercions:}
\begin{definition}
We define: $Coerc = iter^N$ $succ$ $0: N \limpl !N$.
\end{definition}

 We have $Coerc n \rightarrow n$.
 More generally, $Coerc: N \limpl !^i N$, $i\geq 1$, by taking $A=!^{(i-1)} N$ and $succ=!(!^{(i-1)} N \limpl !^{(i-1)} N)$
 Therefore, if $\vdash_{ELL} t: !^{i} N \limpl A$, then $t$ can be replaced with $t'$ representing the same function, with $\vdash t':N \limpl A$. For that, we take $t' = \lambda x.(t (Coerc x))$.

\begin{rmk}
This is why we considered functions of type $N \limpl !^k N$. The same property also holds for the type $W$ and the other data types.
\end{rmk}



% ----------------------------------------------------------------------------------------------------------
% ----------------------------------------------------------------------------------------------------------
% ----------------------------------------------------------------------------------------------------------



\newpage

% ------ Chap 2 : LLL
\section{Light Linear Logic}

\begin{ex}
 Let us consider, for instance double (with an add inside the box and $A=N$):
% TODO: proof-net pour double (sans rien mettre dans la !-box)

 We put $n$ copies one after the others, and we reduce the two last copies:

% TODO: proof-net obtenu après réduction de 2 doubles mis bout à bout.

 Therefore, during reduction, contraction node $i$ eventually creates $2^i$ contraction nodes. So, eventually, $size \geq 2^n$
\end{ex}

\par To avoid this situation, we distinguish two kind of boxes: boxes with at most one auxiliary door, which are duplicable, and boxes with 2 or more auxiliary doors, which are not duplicable. So, we have to introduce a new connective $§$, called \emph{paragraph} (or \emph{neutral}). Thus, we obtain the Light Linear Logic (introduced by Girard in 1995).

\subsection{Light Linear Logic (LLL)}
\par The grammar type of LLL is: $A,B,... \Coloneqq \alpha | A \limpl B | !A | §A | \forall \alpha.A $

\par Its typing rules are the same than in IMLL and ELL for (ax), ($\limpl_i$), ($\limpl_e$), ($\forall_i$) and ($\forall_e$). The (contr) and (weak) rules are the same than in ELL. In addition, we have 4 more rules in LLL which are:\\
$	\infer[(!_i)]{x:!A \vdash t:!B}{x:A \vdash t:B} \quad
	\infer[(!_i)]{\vdash t:!B}{\vdash t:B} \quad
	\infer[(!_e)]{\Gamma_1,\Gamma_2 \vdash u[t/x]:B}{\Gamma_1 \vdash t:!A & x:!A,\Gamma_2 \vdash u:B} \\
	\infer[(§_i), 0\leq k\leq n]{x_1:!A_1, ... ,x_k:!A_k, x_{k+1}:§A_{k+1}, ... ,x_n:§A_n \vdash t: B}{x_1:A_1, ... x_n:A_n \vdash t: B} \quad
	\infer[(§_e)]{\Gamma_1,\Gamma_2 \vdash u[t/x]:B}{\Gamma_1 \vdash t:§A & x:§A,\Gamma_2 \vdash u:B} \quad
$

In particular:
$	\infer[(§_i), k=0]{§\Gamma \vdash t: B}{\Gamma \vdash t: B} \quad
	\infer[(§_i), k=n]{!\Gamma \vdash t: B}{\Gamma \vdash t: B}
$

\begin{ex}
$$ \infer[(\limpl_i)]{\vdash \lambda x.x : !A \limpl §A}{
	\infer[(§_i)]{x:!A \vdash x:§A}{x:A \vdash x:A}
	}
$$
\end{ex}

\par To obtain the Light Affine Logic (LAL), we just have to add to LLL the general weak rule:
$LAL = LLL + \infer[(gen weak)]{§x:A, \Gamma \vdash t: B}{\Gamma \vdash t: B}$

\par We have a forgetfull map $(.)^{o}$ between LLL and ELL which transform every $§$ in a formula into a $!$. Therefore, we have a forgetful map to system F.

\begin{prop}
If $\Gamma \vdash_{LLL}$, then $\Gamma^o \vdash_{ELL} t:A^o$
\end{prop}
\begin{proof}
By induction on the LLL derivation.
\end{proof}


% -----
\subsection{LLL data types}

\begin{center}
\begin{tabular}{|c|c|}
\hline
LLL & ELL \\
\hline
$N^{LLL}=\forall \alpha. !(\alpha \limpl \alpha) \limpl §(\alpha \limpl \alpha)$ & $N^{ELL} = \forall \alpha. !(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha)$\\
\hline
$W^{LLL}=\forall \alpha.!(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha) \limpl §(\alpha \limpl \alpha)$ & $W^{ELL} = \forall \alpha. !(\alpha \limpl \alpha) \limpl !(\alpha \limpl \alpha)$\\
\hline
\end{tabular}
\end{center}

\begin{ex}[Type derivation for $\underbar{2}$]
$$	\infer{\vdash \underbar{2}:N^{LLL}}{
		\infer{\vdash \lambda f x. f f x : !(\alpha \limpl \alpha) \limpl §(\alpha \limpl \alpha)}{
			\infer[(contr)]{f: !(\alpha \limpl \alpha) \vdash \lambda x. f f x : §(\alpha \limpl \alpha)}{
				\infer[(§i)]{f_1,f_2:!(\alpha \limpl \alpha) \vdash \lambda x. f_1 f_2 x:§(\alpha \limpl \alpha)}{
				\infer{f_1,f_2:(\alpha \limpl \alpha) \vdash \lambda x.f_1 f_2 x: \alpha \impl \alpha}{}
				}
			}
		}
	}$$
\end{ex}

\begin{ex}[Examples of typed terms]
\item $add = \lambda n m f x.(n f (m f x)): N^{LLL} \limpl N^{LLL} \limpl N^{LLL}$
\item $double = \lambda n f x.(n f (n f x)): N \limpl § N$
\item $Conc = \lambda w w' s_0 s_1 x.(w s_0 s_1 (w' s_0 s_1 x)) : W \limpl W \limpl W$
\end{ex}

\begin{exo}
Write the type derivation for $add$ in $LLL$.
(Hint: the derivation has the same shape as the one in $ELL$, but we have to replace one $(!_i)$ by a $(§_i)$ and 2 $(!_e)$ by $(§_e)$
\end{exo}

\begin{ex}[Type derivation for double]
$$ \infer{\vdash \lambda k.add k k: !N \limpl §N}{
		\infer{k:!N \vdash add k k: §N}{
			\infer[(contr)]{n:!N, m:!N \vdash add n m :§N}{
			\infer[(§i)]{n:N, m:N \vdash add n m:N}{}
		}
	}
} $$
\end{ex}

 However, $mult$ has not the type $(N \limpl N \limpl N)$ in LLL, but is represented by an other term, which is typable in LLL (intuition: (m f) has a type $§(\alpha \limpl \alpha)$ but $n$ expect an argument of type $§(\alpha \limpl \alpha)$.

\begin{exo}
Give 2 terms representing $Cons_0$ and $Cons_1$, and show that they can be given the type $W \limpl W$.
\end{exo}


% -----
\subsection{Iteration in LLL}
 We define $iter^N = \lambda f x n.(n f x): !(A \limpl A) \limpl §A \limpl N \limpl §A$.

\begin{ex}
We have $add: N \limpl N \impl N$ and $add \underbar{2} : N \limpl N$.
So, $iter^N (add \underbar{2}) \underbar{0} : N \limpl §N $.
$$ \infer{\vdash iter^N (add \underbar{2}) \underbar{0} : N \limpl §N}{
		\infer{\vdash add \underbar{2} : !(N \limpl N)}{
			\infer{\vdash add \underbar{2} : N \limpl N}{}
		}
		&
		\infer{\vdash \underbar{0} : §N}{ \vdash \underbar{0} : N}
	}$$
\end{ex}

\begin{rmk}
If $\Gamma \vdash step: A \limpl A$, one will be able to iterate on $step$ in LLL, only if $step$ has at most one free variable (in order to apply the $(!_i)$ rule.
\end{rmk}

\begin{definition}
Multiplication: $mult' = \lambda n m. iter^N (add n) \underbar{0} m$
$$ \infer{\vdash \lambda n.iter^N (add n) \underbar{0} : !N \limpl N \limpl §N}{
	\infer{ n:!N \vdash iter^N (add n) \underbar{0} : N \limpl §N}{
		\infer{n:!N \vdash add n : !(N \limpl N)}{ n:N \vdash add n : N \limpl N}
	&
		\infer{\vdash \underbar{0} : §N}{ \vdash \underbar{0} : N}
	}
} $$
\end{definition}

\begin{exo}
Write some typed terms representing the following functions on binary words:
$f(<a_1, ..., a_n>) = <\overline{a_1}, ..., \overline{a_n}>$ where $\overline{0}=1$ and $\overline{1}=0$.
$g(<a_1, ..., a_n>) = <a_1, a_1, a_2, a_2, ..., a_n, a_n>$.
Hint: use iteration on binary words: $iter^W= \lambda f_0 f_1 x w.(w f_0 f_1 x) : !(A \limpl A) \limpl !(A \limpl A) \limpl §A \limpl W \limpl §A$.

\end{exo}


% -----
\subsection{LLL proof nets}





% TODO: Continuer...


\end{document}


% FIXME:
% - La preuve complète Chap 1 au niveau de la sous-section "Reduction Stratégie" (il y a un Fixme à cet endroit)
% Attention à l'agencement des figures chap 1 si quelqu'un la rajoute...

